$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, $s$:timedState(${\it ds}$). shift{-}state($s$) $\in$ timedState(${\it ds}$)